Nuprl Lemma : matters_wf
0,22
postcript
pdf
a
:Atom1,
T
:Type,
g
:(
T
),
x
:
T
. AtomFree(Type;
T
)
M(
a
;
g
;
x
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
,
Prop
Lemmas
atom-free
wf
,
bool
wf
origin
a:Atom1, T:Type, g:(T
), x:T. AtomFree(Type;T) 
M(a;g;x) 
a:Atom1, T:Type, g:(T), x:T. AtomFree(Type;T) M(a;g;x) x:A. B(x) Q T